\begin{tabbing}
$\forall$$i$, $a$:Id, $T$:Type, ${\it ds}$:$a$:Id fp$\rightarrow$ Type, $P$:(State(${\it ds}$)$\rightarrow$$T$$\rightarrow$Prop).
\\[0ex]@$i$: (with ds: ${\it ds}$ action $a$:$T$ precondition $a$(v) is $P$ s v) $\in$ Dsys
\\[0ex]\& (\=$\forall$$D$:Dsys.\+
\\[0ex]@$i$: (with ds: ${\it ds}$ action $a$:$T$ precondition $a$(v) is $P$ s v) $\subseteq$ $D$
\\[0ex]$\Rightarrow$ $D$ realizes ${\it es}$. @$i$ Precondition for $a$(v)$P$ State(${\it ds}$) (v:$T$))
\-
\end{tabbing}